\begin{tabbing}
[$e_{1}$;$e_{2}$]$\sim$([$a$,$b$].$p$($a$;$b$))$\ast$[$a$,$b$].$q$($a$;$b$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\exists$$m$:$\mathbb{N}^{+}$, $f$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$$\rightarrow$\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) \}).\+
\\[0ex]$f$(0) $=$ $e_{1}$ \& $f$($m$$-$1) $\leq$ $e_{2}$ 
\\[0ex]\& ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$m$$-$1}}$. ($f$($i$) $<$loc $f$($i$+1))) \& ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$m$$-$1}}$. $p$($f$($i$);pred($f$($i$+1))))
\\[0ex]\& $q$($f$($m$$-$1);$e_{2}$)
\-
\end{tabbing}